/**
 * 
 */
package edu.arizona.bio5.onto.decomposition.locality;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.Set;

import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLClassExpression;
import org.semanticweb.owlapi.model.OWLClassExpressionVisitor;
import org.semanticweb.owlapi.model.OWLDataAllValuesFrom;
import org.semanticweb.owlapi.model.OWLDataExactCardinality;
import org.semanticweb.owlapi.model.OWLDataHasValue;
import org.semanticweb.owlapi.model.OWLDataMaxCardinality;
import org.semanticweb.owlapi.model.OWLDataMinCardinality;
import org.semanticweb.owlapi.model.OWLDataSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLEntity;
import org.semanticweb.owlapi.model.OWLObjectAllValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectComplementOf;
import org.semanticweb.owlapi.model.OWLObjectExactCardinality;
import org.semanticweb.owlapi.model.OWLObjectHasSelf;
import org.semanticweb.owlapi.model.OWLObjectHasValue;
import org.semanticweb.owlapi.model.OWLObjectIntersectionOf;
import org.semanticweb.owlapi.model.OWLObjectMaxCardinality;
import org.semanticweb.owlapi.model.OWLObjectMinCardinality;
import org.semanticweb.owlapi.model.OWLObjectOneOf;
import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectUnionOf;

import uk.ac.manchester.cs.util.SetUtils;

import com.clarkparsia.owlapi.modularity.locality.LocalityClass;

/**
 * Given a locality class "x" and a signature S, computes all
 * minimal (w.r.t. inclusion) subsets of S s.t. the given class expression C
 * does not belong to Top(S)

 * See the paper "Which kind of module should I extract" by T. Schneider et al.
 * 
 * @author Pavel Klinov
 *
 */
public class TopNonEquivFinder implements OWLClassExpressionVisitor {

	private LocalityClass m_localClass = null;
	private Collection<Set<OWLEntity>> m_minSubsigs = null;
	private Collection<? extends OWLEntity> m_sig = null;
	
	TopNonEquivFinder(LocalityClass lClass) {
		
		m_localClass  = lClass;
	}

	/*
	 * Shouldn't be called recursively on the same instance
	 */
	public Collection<Set<OWLEntity>> findMinimalSignatures(OWLClassExpression clazz, Collection<? extends OWLEntity> signature) {
		
		m_sig = signature;
		m_minSubsigs = new ArrayList<Set<OWLEntity>>();
		clazz.accept(this);
		
		return m_minSubsigs;
	}

	@Override
	public void visit(OWLClass clazz) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        	// The class is never in Top(S) unless it is Thing 
        	if (!clazz.isOWLThing()) LocalityUtils.saveEmptySignature(m_minSubsigs);
        		
            break;
        case TOP_BOTTOM:
        case TOP_TOP:
        	
        	//isTopEquivalent = desc.isOWLThing() || (!desc.isOWLNothing() && !signature.contains(desc));
        	if (!clazz.isOWLThing()) {
        		// If the class is Nothing it is obviously not in Top(S) for any signature
            	if (clazz.isOWLNothing()) {
            		
            		LocalityUtils.saveEmptySignature(m_minSubsigs);
            		
            	} else {
            		//The class is not in Top(S) for all S that contain its name
            		LocalityUtils.saveName(clazz, m_sig, m_minSubsigs);
            	}
        	}
		}
	}

	@Override
	public void visit(OWLObjectIntersectionOf clazz) {
		// Find all signatures S s.t. at least one conjunct is not in Top(S)
		for (OWLClassExpression conjunct : clazz.getOperands()) {
			// Find minimal subsignatures recursively for each conjunct 
			Collection<Set<OWLEntity>> minSigsForConjunct = new TopNonEquivFinder(m_localClass).findMinimalSignatures(conjunct, m_sig);
			
			SetUtils.addAllandMinimizeWrtInclusion(minSigsForConjunct, m_minSubsigs);
		}
	}

	@Override
	public void visit(OWLObjectUnionOf clazz) {
		//TODO Optimize. Need a data structure to maintain all sets minimal w.r.t. inclusion (i.e., incomparable)
		m_minSubsigs = null;
		// *All* disjuncts must not be in Top(S)
		for (OWLClassExpression disj : clazz.getOperands()) {

			Collection<Set<OWLEntity>> minSigsForDisjunct = new TopNonEquivFinder(m_localClass).findMinimalSignatures(disj, m_sig);
			// Combine the new signatures with signatures that push the previous disjuncts out of Top(S)
			m_minSubsigs = m_minSubsigs == null ? minSigsForDisjunct : SetUtils.unionAllAndMinimizeWrtInclusion(m_minSubsigs, minSigsForDisjunct);
			
			if (m_minSubsigs.isEmpty()) break;
		}
	}

	@Override
	public void visit(OWLObjectComplementOf clazz) {
		// Find all such signatures S that the operand is not in Bot(S)
		SetUtils.addAllandMinimizeWrtInclusion(new BottomNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getOperand(), m_sig), m_minSubsigs);
	}

	@Override
	public void visit(OWLObjectSomeValuesFrom clazz) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// Here the class is never in Top(S)
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	// Here we need all signatures S s.t.
        	// They contain the property name
        	// OR
        	// The filler is not in Top(S)
        	SetUtils.addAllandMinimizeWrtInclusion(new TopNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig), m_minSubsigs);

        	if (m_sig.contains(clazz.getProperty().getNamedProperty())) {
            	// Add the singleton for the property name        		
        		Set<OWLEntity> prop = Collections.singleton((OWLEntity)clazz.getProperty().getNamedProperty());
        		
        		SetUtils.addAllandMinimizeWrtInclusion(new HashSet<Set<OWLEntity>>(Collections.singleton(prop)), m_minSubsigs);
        	}

            break;
		}
	}

	@Override
	public void visit(OWLObjectAllValuesFrom clazz) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// Here we need all signatures S s.t.
        	// They contain the property name
        	// AND
        	// The filler is not in Top(S)
        	if (m_sig.contains(clazz.getProperty().getNamedProperty())) {
    		
        		m_minSubsigs = 	SetUtils.unionAndMinimizeWrtInclusion(
    							new TopNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig),
    							LocalityUtils.getSingletonSignature(clazz.getProperty().getNamedProperty()));
        	}
            break;
        case TOP_TOP:
        	// Save all signatures S s.t. the filler is not in Top(S)
        	m_minSubsigs = new TopNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig);
            break;
    }
	}

	@Override
	public void visit(OWLObjectHasValue clazz) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// The class is never in Top(S) here
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	// The class is not in Top(S) w.r.t. all S that contain the name of the property
        	LocalityUtils.saveName(clazz.getProperty().getNamedProperty(), m_sig, m_minSubsigs);
        	
            break;
        }
	}

	@Override
	public void visit(OWLObjectMinCardinality clazz) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	if (clazz.getCardinality() > 0) {
        		//Here the class can't be in Top
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        	}
            break;
        case TOP_TOP:
        	
        	if (clazz.getCardinality() > 0) {
        		//Otherwise the class is always in Top(S)
        		// Find all S s.t. it contains the property name OR the filler is not in Top(S)
        		m_minSubsigs = new TopNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig);
            	
        		if (m_sig.contains(clazz.getProperty().getNamedProperty())) {
                	// Add the singleton for the property name        		
            		Set<OWLEntity> prop = Collections.singleton((OWLEntity)clazz.getProperty().getNamedProperty());
            		
            		SetUtils.addAllandMinimizeWrtInclusion(new HashSet<Set<OWLEntity>>(Collections.singleton(prop)), m_minSubsigs);
            	}
        	}
		}
	}

	@Override
	public void visit(OWLObjectExactCardinality clazz) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	
        	if (clazz.getCardinality() == 0) {
        		// Find all S s.t.
        		// S contains the property name
        		// AND
        		// the filler is not in Bot(S)
        		m_minSubsigs = 	SetUtils.unionAndMinimizeWrtInclusion(
        							new BottomNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig),
        							LocalityUtils.getSingletonSignature(clazz.getProperty().getNamedProperty()));
        		
        	} else {//Never in Top(S) here
        		
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        	}
        	
            break;
        case TOP_TOP:
        	
        	if (clazz.getCardinality() == 0) {
        		// The filler must not be in Bot(S)
        		m_minSubsigs = new BottomNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig);
        		
        	} else {//Never in Top(S) here
        		
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        	}
        }		
	}

	@Override
	public void visit(OWLObjectMaxCardinality clazz) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// Find all S s.t. it contains the property name AND the filler is not in Bot(S)
    		if (m_sig.contains(clazz.getProperty().getNamedProperty())) {
    			
    			m_minSubsigs =	new BottomNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig);
    			m_minSubsigs = 	SetUtils.unionAndMinimizeWrtInclusion(m_minSubsigs,	LocalityUtils.getSingletonSignature(clazz.getProperty().getNamedProperty()));
        	}

            break;
        case TOP_TOP:
        	// The filler must not be in Bot(S)
    		m_minSubsigs = new BottomNonEquivFinder(m_localClass).findMinimalSignatures(clazz.getFiller(), m_sig);
            break;
		}
	}

	@Override
	public void visit(OWLObjectHasSelf clazz) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// The class is never in Top here
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	// The subsignatures need to contain the property name
        	LocalityUtils.saveName(clazz.getProperty().getNamedProperty(), m_sig, m_minSubsigs);
            break;
        }		
	}

	@Override
	public void visit(OWLObjectOneOf clazz) {
		// The class is never in Top here
		LocalityUtils.saveEmptySignature(m_minSubsigs);
	}

	@Override
	public void visit(OWLDataSomeValuesFrom clazz) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// The class is never in Top here
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	// Find all S s.t. it contains the property name OR the filler is neither top datatype nor a built-in
    		if (!LocalityUtils.isTopOrBuiltInDatatype(clazz.getFiller())) {
    			// The class is not in Top here
    			LocalityUtils.saveEmptySignature(m_minSubsigs);
            	
    		} else {
    			
    			LocalityUtils.saveName(clazz.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
    		}
		}
	}

	@Override
	public void visit(OWLDataAllValuesFrom clazz) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:

        	if (!clazz.getFiller().isTopDatatype()) {
        		// The class is not in Top(S) if S contains the property name
        		LocalityUtils.saveName(clazz.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        	}

            break;
        case TOP_TOP:
        	
        	if (!clazz.getFiller().isTopDatatype()) {
        		// The class is not in Top here
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        	}
		}
	}

	@Override
	public void visit(OWLDataHasValue clazz) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// The class is not in Top here
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	// The class is not in Top(S) if S contains the property name
        	LocalityUtils.saveName(clazz.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
            break;
        }		
	}

	@Override
	public void visit(OWLDataMinCardinality clazz) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	
        	if (clazz.getCardinality() > 0) {
        		//Never in Top(S) here
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        	}

            break;
        case TOP_TOP:
        	
        	if (clazz.getCardinality() > 0) {//If the cardinality is 0 then the class is always in Top(S)

    			if ((clazz.getCardinality() != 1 
    						||	!LocalityUtils.isTopOrBuiltInDatatype(clazz.getFiller()))
    				&&
    				(clazz.getCardinality() <= 1
    						|| !LocalityUtils.isTopOrBuiltInInfiniteDatatype(clazz.getFiller()))) {
    				//If we are here then the class can't be in Top(S)
    				LocalityUtils.saveEmptySignature(m_minSubsigs);	
    				
    			} else {
    				// The class is not in Top(S) for any S that contains the property name
    				LocalityUtils.saveName(clazz.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
    			}
			}
        	
        	/*isTopEquivalent = desc.getCardinality() == 0 
        						|| (desc.getCardinality() == 1 && !signature.contains(desc.getProperty().asOWLDataProperty()) && LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller()))
        						|| (desc.getCardinality() > 1 && !signature.contains(desc.getProperty().asOWLDataProperty()) && LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller()));*/
        }		
	}

	@Override
	public void visit(OWLDataExactCardinality clazz) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	
        	if (clazz.getCardinality() > 0) {
        		// Here the class is never in Top(S)
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
    			
        	} else {
        		// The class is not in Top is the signature contains the property name
        		LocalityUtils.saveName(clazz.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        	}

            break;
        case TOP_TOP:
        	// Here the class is never in Top(S)
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
        }
	}

	@Override
	public void visit(OWLDataMaxCardinality clazz) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// The signature must contain the property name
        	LocalityUtils.saveName(clazz.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
            break;
        case TOP_TOP:
        	// Here the class is never in Top(S)
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        }		
	}	
}
